module counter_props (
    input wire clk,
    input wire rst_n,
    input wire en,
    input wire [3:0] cnt,
    input wire ovf
);
    //                
    reg [3:0] past_cnt;
    reg [3:0] past_cnt_delayed;  //                               cnt   
    reg error_p_rst;
    reg error_p_cnt_auto_inc;
    reg error_p_reset_ovf;

    //                
    always @(posedge clk) begin
        past_cnt <= cnt;
        past_cnt_delayed <= past_cnt;  //                
    end

    // ==============================================
    //       1:                                                 
    //       SVA: !rst_n |=> (cnt == 0 && !ovf)
    // ==============================================
    always @(posedge clk) begin
        if (!rst_n) begin
            //                                                       
            error_p_rst <= 1'b1;
        end else begin
            //                                        
            if (error_p_rst) begin
                if (cnt != 4'b0 || ovf != 1'b0) begin
                    $error("[SVA FAIL] p_rst: cnt=%0d ovf=%0d at %t", cnt, ovf, $time);
                end
                error_p_rst <= 1'b0;
            end
        end
    end

    // ==============================================
    //       2:                                           
    //       SVA: en && (cnt < 4'hf) |=> cnt == past_cnt + 1
    // ==============================================
    always @(posedge clk) begin
        if (en && (past_cnt < 4'hf)) begin
            //                            
            if (cnt != (past_cnt + 1'b1)) begin
                $error("[SVA FAIL] p_cnt_auto++: expected=%0d actual=%0d at %t",
                      (past_cnt + 1'b1), cnt, $time);
                error_p_cnt_auto_inc <= 1'b1;
            end
        end
        //                               
        error_p_cnt_auto_inc <= 1'b0;
    end

    // ==============================================
    //       3:                                           
    //       SVA: en && (past_cnt == 4'hf) |=> (cnt == 0 && ovf)
    // ==============================================
    always @(posedge clk) begin
        if (en && (past_cnt_delayed == 4'hf)) begin
            if (cnt != 4'b0 || ovf != 1'b1) begin
                $error("[SVA FAIL] p_reset_ovf: cnt=%0d ovf=%0d at %t", cnt, ovf, $time);
                error_p_reset_ovf <= 1'b1;
            end
        end
        //                               
        error_p_reset_ovf <= 1'b0;
    end

    // ==============================================
    //                                     
    // ==============================================
    generate
        for (genvar i = 0; i < 16; i++) begin : gen_covers
            always @(posedge clk) begin
                if (cnt == i) begin
                    $display("[COVER] cnt=%0d at %t", i, $time);
                end
            end
        end
    endgenerate

endmodule